(**
 * @copyright (C) 2021 SML# Development Team.
 * @author UENO Katsuhiro
 *)
include "../../../libs/ids/main/LocalID.smi"
include "../../../data/types/main/Types.ppg.smi"
include "../../../compilerIRs/recordcalc/main/RecordCalc.ppg.smi"
include "../../../compilerIRs/recordcalc/main/RecordCalc.ppg.smi"

signature KIND_INSTANCE =
sig

  (* the body of the singleton type term that this module deals with. *)
  type singleton_ty_body

  (* the type of kind that this module deals with. *)
  type kind

  (* the type of instance; in almost cases, it should be RecordCalc.rcexp *)
  type instance

  (* the singleton type constructor *)
  val singletonTy
      : singleton_ty_body -> Types.singletonTy

  (* generate the singleton types of the extra arguments of the given kind *)
  val generateArgs
      : Types.btvEnv
        -> BoundTypeVarID.id * kind
        -> Types.singletonTy list

  (* compare two singleton types generated by generateArgs *)
  val compare
      : singleton_ty_body * singleton_ty_body -> order

  (* generate the unique instance of the given singleton type if it exists *)
  val generateInstance
      : {lookup : Types.singletonTy -> RecordCalc.varInfo option,
         btvEnv : Types.btvEnv}
        -> singleton_ty_body
        -> RecordCalc.loc
        -> instance option

end
